Nuprl Definition : binrel_eqv
13,42
postcript
pdf
E
<
>{
T
}
E'
==
x
,
y
:
T
. (
E
(
x
,
y
))
(
E'
(
x
,
y
))
latex
clarification:
E
<
>{
T
}
E'
==
x
:
T
,
y
:
T
. (
E
(
x
,
y
))
(
E'
(
x
,
y
))
latex
Up
gen
algebra
1
Wellformedness Lemmas
binrel
eqv
wf
Definitions
x
:
A
.
B
(
x
)
,
P
Q
origin
>{T} E' == 
x, y:T. (E(x,y)) 
(E'(x,y))
>{T} E' == x:T, y:T. (E(x,y)) (E'(x,y)) >{T} E' == x, y:T. (E(x,y)) (E'(x,y))
>{T} E' == x:T, y:T. (E(x,y)) (E'(x,y)) x:A. B(x) Q